es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;i)))
 (e:E.
 (loc(e) = i)
  (kind(e)  dom(conds))
  ((valtype(e) r (conds(kind(e)).1)) & (state@loc(e) r State(ds))))
 (e:E. ((e  es-triggers(es;i;ds;conds)))  (loc(e) = i)) 

latex

Definitions	x:A. B(x), a:A fp B(a), P  Q, P & Q, t  T, , x:A. B(x), A c B, x. t(x), Top, b, Dec(P), P  Q, ff, if b then t else f fi , False, x(s)
Lemmas	decidable equal Id, assert wf, es-is-interface wf, es-triggers wf, fpf-dom wf, es-E wf, Id wf, es-loc wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, decl-state wf, top wf, es-kind wf, es-valtype wf, pi1 wf, fpf-ap wf, es-state wf, hasloc wf, l member wf, event system wf, es-triggers-not-loc